a, b:. ((a b) ~ ff)  {(a ~ ff) & (b ~ ff)} 

latex

ProofTree

Definitions	SQType(T), {T}, left + right, Unit, P  Q, x:A  B(x), x:AB(x), , , s = t, b, A, b, x:A. B(x), t  T, P  Q, s ~ t, P & Q
Lemmas	assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool wf